| Model: | ftwc v.3 (MA) |
| Parameter(s) | N = 8, TIME_BOUND = 5 |
| Property: | TimeMin (exp-time) |
~/storm/build/bin/storm --jani ftwc.jani --janiproperty TimeMin --constants N=8,TIME_BOUND=5 --timebounded:precision 1e-3 --engine portfolio --ddlib sylvan --sylvan:maxmem 6114 --sylvan:threads 4
| Walltime: | 0.15390300750732422s |
| Return code: | 0 |
| Note(s): | The tool result '2005997773/1000' is tagged as incorrect. The reference result is '49569188244691157640777897241488668673626828644189196764038763495934127772581818827657586026182066161989586432749290712194700462126341074934150546100723871655022185670368170152617720178361433722295645619967358084478494099834546378515936142056456021598789834283048399401085339317779160390335682147332083362300224412076816495866312174143937455974191483876650634293062037795776270685493296644510209669509237851584765684566319405462211776204286741525848384633073583969430572762424515151621071750667235423403758187586317061236078533181354878564558387588980534648853069632194739724249745082550820673689600851494125098336522102029348889315394356316567042690867241625261321753876969463822917919195565785841792738462060644802994850536051247180583737651569809934874977339480766075664244250332086771357685540617282828501673946775997764669305736487039689172341089365623671489365717826320627382322103417725112433594282348889076090944230945406554918527903586582075043048674014511775664428763679569460522578957195093204969068885918475954701981402654127272466212590205273467564862315724959246929444124634711891552506708340148443800560671281541666269819810615151079332224771479495605749007741738092305482664765071171188083874586957347417508650944279607451563868631260391999681051953256273570589614525154845090948500816094914209009712314266308932240145318038518254540637911577676498155054493673673322363318272452913909409954810049120798288862526997108335418019182140484143216503177367680163525695647392660591226665498917649041525209344406718195961721470760740289700558365483413406314301238058452518910989373505461571250706410608116754534657620512043545742686327075556074969531847055414282142342990587271158113524384810692830321875392616737551359026591315526253863159107359791046537161916908190887590221726345491223571497457986130346683481045292688213449727577039326510222012881402702075807120/24842480089988447240790617968641731326940011285882082728179896138423523367936760021370104561829991319957969724182256554425167446318631445950695892190402200836787387825155296486116781062019218601643410100142338505175042674102424627326985770121516822573795411953828822495761575522151561445549403085550785674313461919668355506791088789501834828697680745307151308323681304495965293483776759303307260636277363175284409815738275729579884513414133969667756339462005963610505631087075363687809962404734200149292991785208958801489793636767017334885872786774677826308936498950592119270646451579725797475568214721614617543921340306589538760150278878465396260176691820614575734157703329470399589957386076277139682713044193347334676400310427293961340032044853283332077959111706619134528827537788327134939782541587456360768634523647132311813576410650991163357018897462476294723921890820274571494991217501269601816908351375125936826784571099088551243742036837407584471455136531016695810076672064640322257880612919897434991437719737996503119899441329003804923403751422819820661775082756378482159004005829507361729274693612684741636552544024653448109238047025949136815529375658991993266253110622081321025838624126453055551758039028171267383158887476201289629124095280666902919443923213711890766831606926524195878661782192061815893415105317562221779731297712719333522448927790537703584926982226192215421677660470272113138984504066019788276425859009119389029354552006489918430035857810365628253511760413105497853130919105042626582736098208254848720104572120600608729116426288869899829856901833423746811338914270544621210968972627535306289365445761466299769041279947528407598940212566703547006078502616697208674580830606531520061155353505169548249135604202264576558988956723219864209825965891779696849654064191030724636930430924643971545682008428417071282354575536083253622140884212063927' (approx. 1995339.7593611279) which means a relative error of '0.005341453047717885' which is larger than the goal precision '0.001'. |
| Relative Error: | 0.005341453047717885 |
Storm 1.5.1 Date: Thu Mar 19 00:42:48 2020 Command line arguments: --jani ftwc.jani --janiproperty TimeMin --constants 'N=8,TIME_BOUND=5' '--timebounded:precision' 1e-3 --engine portfolio --ddlib sylvan '--sylvan:maxmem' 6114 '--sylvan:threads' 4 Current working directory: / Time for model input parsing: 0.003s. Portfolio engine picked the following settings: engine=sparse bisimulation=false exact=false Time for model construction: 0.096s. -------------------------------------------------------------- Model type: Markov Automaton (sparse) States: 10299 Transitions: 26983 Choices: 12635 Markovian St.: 4951 Max. Rate.: 2.0307 Reward Models: none State Labels: 3 labels * deadlock -> 0 item(s) * (((workstations_up[0] = 0) | switches_down[0]) & ((workstations_up[1] = 0) | switches_down[1])) -> 1059 item(s) * init -> 1 item(s) Choice Labels: none -------------------------------------------------------------- Time for model preprocessing: 0.000s. -------------------------------------------------------------- Model type: Markov Automaton (sparse) States: 10299 Transitions: 26983 Choices: 12635 Markovian St.: 4951 Max. Rate.: 2.0307 Reward Models: none State Labels: 3 labels * deadlock -> 0 item(s) * (((workstations_up[0] = 0) | switches_down[0]) & ((workstations_up[1] = 0) | switches_down[1])) -> 1059 item(s) * init -> 1 item(s) Choice Labels: none -------------------------------------------------------------- Model checking property "TimeMin": T[exp]min=? [F (((workstations_up[0] = 0) | switches_down[0]) & ((workstations_up[1] = 0) | switches_down[1]))] ... Result (for initial states): 2005997.773 Time for model checking: 0.024s.